\begin{tabbing}
R{-}frame{-}compat($A$; $B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Reffect?($A$)\+\+
\\[0ex]then \=if\= Rframe?($B$)\+\+
\\[0ex]then \=(Rframe{-}x($B$) = Reffect{-}x($A$) $\in$ Id)\+
\\[0ex]$\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]if\= Raframe?($B$)\+
\\[0ex]then \=(Raframe{-}k($B$) = Reffect{-}knd($A$) $\in$ Knd)\+
\\[0ex]$\Rightarrow$ (Reffect{-}x($A$) $\in$ Raframe{-}L($B$) $\in$ Id)
\-\-\\[0ex]if\= Rrframe?($B$)\+
\\[0ex]then \=($\uparrow$fpf{-}dom(id{-}deq; Rrframe{-}x($B$); Reffect{-}ds($A$)))\+
\\[0ex]$\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]if\= Rsends?($A$)\+
\\[0ex]then \=if\= Rsframe?($B$)\+\+
\\[0ex]then \=(Rsframe{-}lnk($B$) = Rsends{-}l($A$) $\in$ IdLnk)\+
\\[0ex]$\Rightarrow$ (Rsframe{-}tag($B$) $\in$ map(($\lambda$$p$.$p$.1); Rsends{-}g($A$)) $\in$ Id)
\\[0ex]$\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rsframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]if\= Rbframe?($B$)\+
\\[0ex]then \=(Rbframe{-}k($B$) = Rsends{-}knd($A$) $\in$ Knd)\+
\\[0ex]$\Rightarrow$ (Rsends{-}l($A$) $\in$ Rbframe{-}L($B$) $\in$ IdLnk)
\-\-\\[0ex]if\= Rrframe?($B$)\+
\\[0ex]then \=($\uparrow$fpf{-}dom(id{-}deq; Rrframe{-}x($B$); Rsends{-}ds($A$)))\+
\\[0ex]$\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]if\= Rpre?($A$)\+
\\[0ex]then \=if Rrframe?($B$)\+
\\[0ex]then \=($\uparrow$fpf{-}dom(id{-}deq; Rrframe{-}x($B$); Rpre{-}ds($A$)))\+
\\[0ex]$\Rightarrow$ (locl(Rpre{-}a($A$)) $\in$ Rrframe{-}L($B$) $\in$ Knd)
\-\\[0ex]else True
\\[0ex]fi 
\-\-\\[0ex]else True
\\[0ex]fi 
\-
\end{tabbing}